The Infona portal uses cookies, i.e. strings of text saved by a browser on the user's device. The portal can access those files and use them to remember the user's data, such as their chosen settings (screen view, interface language, etc.), or their login data. By using the Infona portal the user accepts automatic saving and using this information for portal operation purposes. More information on the subject can be found in the Privacy Policy and Terms of Service. By closing this window the user confirms that they have read the information on cookie usage, and they accept the privacy policy and the way cookies are used by the portal. You can change the cookie settings in your browser.
Yuri Gurevich was born on May 7, 1940, in Nikolayev, Ukraine, which was a part of Soviet Union at the time. A year later, World War II reached the Soviet Union, and Yuri’s father was assigned to work in a tank body factory near Stalingrad. So that’s where Yuri spent the second year of his life, until the battle of Stalingrad forced the family, except for his father, to flee. Their home was destroyed...
Yuri Gurevich made many varied and deep contributions to logic for computer science. Logic provides also the theoretical foundation of database systems. Hence, it is almost unavoidable that Gurevich made some great contributions to database theory. We discuss some of these contributions, and, along the way, present some personal anecdotes connected to Yuri and the author. We also describe the honorary...
In this case study we describe an approach to a general logical framework for tracking evidence within epistemic contexts. We consider as basic an example which features two justifications for a true statement, one which is correct and one which is not. We formalize this example in a system of Justification Logic with two knowers: the object agent and the observer, and we show that whereas the object...
We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic Kripke-style semantics. We show that every strict constructive canonical system induces a class of non-deterministic Kripke-style frames, for which...
Let $M=(A,<,\overline{P})$ where (A, < ) is a linear ordering and denotes a finite sequence of monadic predicates on A. We show that if A contains an interval of order type ω or − ω, and the monadic second-order theory of M is decidable, then there exists a non-trivial expansion M′ of M by a monadic predicate such that the monadic second-order theory of M′ is still decidable.
When one views (multi-sorted) existential fixed-point logic (EFPL) as a database query language, it is natural to extend it by allowing universal quantification over certain sorts. These would be the sorts for which one has the “closed-world” information that all entities of that sort in the real world are represented in the database. We investigate the circumstances under which this extension of...
Over the past two decades, Gurevich and his colleagues have developed axiomatic foundations for the notion of algorithm, be it classical, interactive, or parallel, and formalized them in a new framework of abstract state machines. Recently, this approach was extended to suggest axiomatic foundations for the notion of effective computation over arbitrary countable domains. This was accomplished in...
The Büchi acceptance condition specifies a set α of states, and a run is accepting if it visits α infinitely often. The co-Büchi acceptance condition is dual, thus a run is accepting if it visits α only finitely often. Nondeterministic Büchi automata over words (NBWs) are strictly more expressive than nondeterministic co-Büchi automata over words (NCWs). The problem of the blow-up involved in the...
We compare the control structures of Abstract State Machines (in short ASM) defined by Yuri Gurevich and AsmL, a language implementing it. AsmL is not an algorithmically complete language, as opposed to ASM, but it is closer to usual programming languages allowing until and while iterations and sequential composition. We here give a formal definition of AsmL, its semantics, and we construct, for each...
We describe our progress building the program ReductionFinder, which uses off-the-shelf SAT solvers together with the Cmodels system to automatically search for reductions between decision problems described in logic.
In a paper published in 1988, Yuri Gurevich gave a precise mathematical formulation of the central question in descriptive complexity - is there a logic capturing P - and conjectured that the answer is no. In the same paper, he also conjectured that there was no logic capturing either of the complexity classes NP ∩ co − NP and RP, and presented evidence for these conjectures based on the construction...
In this paper we use fixed point tilings to answer a question posed by Michael Hochman and show that every one-dimensional effectively closed subshift can be implemented by a local rule in two dimensions. The proof uses the fixed-point construction of an aperiodic tile set and its extensions.
In this paper, we survey results related to the model checking problem for second-order logic over classes of finite structures, including word structures (strings), graphs, and trees, with a focus on prefix classes, that is, where all quantifiers (both first- and second-order ones) are at the beginning of formulas. A complete picture of the prefix classes defining regular and non-regular languages...
In [9] Yuri Gurevich addresses the question whether there is a logic that captures polynomial time. He conjectures that there is no such logic. He considers a logic, we denote it by L ≤ , that allows to express precisely the polynomial time properties of structures; however, apparently, there is no algorithm “that given an L ≤ -sentence ϕ produces a polynomial time Turing machine...
One of the obstacles in automatic program proving is to obtain suitable loop invariants. The invariant of a loop is a weakened form of its postcondition (the loop’s goal, also known as its contract); the present work takes advantage of this observation by using the postcondition as the basis for invariant inference, using various heuristics such as “uncoupling” which prove useful in many important...
We show that lambda calculus is a computation model which can step by step simulate any sequential deterministic algorithm for any computable function over integers or words or any datatype. More formally, given an algorithm above a family of computable functions (taken as primitive tools, i.e., kind of oracle functions for the algorithm), for every constant K big enough, each computation step of...
The question of whether there is a logic that captures polynomial time was formulated by Yuri Gurevich in 1988. It is still wide open and regarded as one of the main open problems in finite model theory and database theory. Partial results have been obtained for specific classes of structures. In particular, it is known that fixed-point logic with counting captures polynomial time on all classes of...
The 11th century Arabic-Persian logician Ibn Sīnā (Avicenna) in Sect. 9.6 of his book Qiyās gives what appears to be a proof search algorithm for syllogisms. We confirm that it is indeed a proof search algorithm, by extracting all the essential ingredients of an Abstract State Machine from Ibn Sīnā’s text. The paper also contains a translation of the passage from Ibn Sīnā’s Arabic, and some notes...
Set the date range to filter the displayed results. You can set a starting date, ending date or both. You can enter the dates manually or choose them from the calendar.